Nuprl Lemma : test-spec-feasible
11,40
postcript
pdf
R-Feasible{i:l}
R-Feasible
(es-realizer(TERMOF{
test-spec
:ObjectId,
R-Feasible(es-realizer(TERMOF{
done:ut2,
R-Feasible(es-realizer(TERMOF{
tg:ut2,
R-Feasible(es-realizer(TERMOF{
b:ut2,
R-Feasible(es-realizer(TERMOF{
done1:ut2,
R-Feasible(es-realizer(TERMOF{
1:ut2,
R-Feasible(es-realizer(TERMOF{
loc2:ut2,
R-Feasible(es-realizer(TERMOF{
loc1:ut2,
R-Feasible(es-realizer(TERMOF{
\\v:l,
R-Feasible(es-realizer(TERMOF{
i:l}))
latex
Definitions
Id
,
t
T
,
normal-type{i:l}(
T
)
,
IdLnk
,
implies-es-real
,
mkid{$x:ut2}
,
send-once-realizable
,
mklnk{$a:ut2, $b:ut2, $n:ut2}
,
test-spec
,
t
.1
,
es-realizer(
p
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
bool-inhabited
,
bool
wf
,
send
onceR
feasible
origin
T, normal-type{i:l}(T), IdLnk, implies-es-real, mkid{$x:ut2}, send-once-realizable, mklnk{$a:ut2, $b:ut2, $n:ut2}, test-spec, t.1, es-realizer(p), P 
Q, 
x:A. B(x)